i1, i2, j1, j2:. (i1  j1)  (i2  j2)  ((i1 * i2)  (j1 * j2)) 

latex

Up	int 2, int 2
Definitions	t  T, P  Q, x:A. B(x), False, A, A  B, ,
Lemmas	nat wf, le wf, mul preserves le